Nuprl Definition : uni_sat
9,38
postcript
pdf
a
= !
x
:
T
.
Q
(
x
) ==
Q
(
a
)
(
a'
:
T
.
Q
(
a'
)
(
a'
=
a
))
latex
clarification:
a
= !
x
:
T
.
Q
(
x
) ==
Q
(
a
)
(
a'
:
T
.
Q
(
a'
)
(
a'
=
a
T
))
latex
Definitions
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
FDL editor aliases
uni_sat
origin
(
a':T. Q(a') 
(a' = a))
(a':T. Q(a') (a' = a 
T)) (a':T. Q(a') (a' = a))
(a':T. Q(a') (a' = a T)) Qx:A. B(x) Q